the_w:World, l:IdLnk, i:Id, a:Action(i). isrcv(l;a)   

latex

Definitions	isnull(a), isrcv(k), kind(a), Action(i), Id, IdLnk, World, isrcv(l;a), p  q, Unit, P  Q, P & Q, , Prop, b, A, b, a = b, lnk(k), x:A. B(x), P  Q, t  T, false
Lemmas	bfalse wf, w-kind wf, lnk wf, eq lnk wf, isrcv wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, w-isnull wf, world wf, IdLnk wf, Id wf, w-action wf